$\forall$$T$:Type. 
\\[0ex]subtype\_rel($T$; $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$, $L$:($T$ List). sorted($L$) $\Rightarrow$ no\_repeats($T$; $L$) $\Rightarrow$ no\_repeats($T$; s{-}insert($x$; $L$)))